\begin{tabbing}
$\forall$$D$:Dsys.
\\[0ex]Feasible($D$)
\\[0ex]$\Rightarrow$ (\=$\forall$${\it dec}$:($i$,$a$:Id$\rightarrow$M($i$).state$\rightarrow$(M($i$).da(locl($a$))+Unit)), $i$:Id.\+
\\[0ex]d{-}machine($i$;M($i$);${\it dec}$($i$))
\\[0ex]$\in$ w{-}automaton($\lambda$$x$.M($i$).ds($x$);$\lambda$$a$.M($i$).da(locl($a$));$\lambda$$l$,${\it tg}$. M(source($l$)).dout($l$,${\it tg}$)))
\-
\end{tabbing}